package ca.shojaei.mini_sat;


import java.util.*;

public class ExistsNext extends Clause {
	
	private Clause F;
	private String symbol = "e@";
	
	public ExistsNext() {
		super();
		this.evaluable = true;
		this.unary = true;
	}
	public ExistsNext(Clause f, String symbol) {
		super();
		F = f;
		this.symbol = symbol;
		this.unary = true;
	}
	
	public Clause getLeft(){
		return getF();
	}
	public void setLeft(Clause c){
		setF(c);
	}
	
	public Clause getRight(){
		return null;
	}
	public void setRight(Clause c){
		;
	}
	
	public Clause getF() {
		return F;
	}
	public void setF(Clause f) {
		F = f;
	}
	
	
	public String getSymbol() {
		if(this.negated){
			String str = "!".concat(this.symbol);
			return str;
		}
		return symbol;
	}
	public void setSymbol(String symbol) {
		this.symbol = symbol;
	}
	
	public boolean evaluate(Model m)
	{
		boolean out = false;
		State cur = m.getCurrentStat();
		Vector<State> nexts = cur.getNexts();
		
		for(int i = 0; i < nexts.size(); i++)
		{
			m.setCurrentStat(nexts.get(i).getStateName());
			if(F.evaluate(m))
			{
				m.setCurrentStat(cur.getStateName());
				out = true;
				break;
			}
				
		}
		
		if(this.negated)
			out = !out;
		
		return out;
		/*boolean out;
		try{
		   out = SAT.isSat(this.getDIMACS(m)) ;
		}catch(Error ex)
		{
			//System.out.println(ex.m)
			return false;
		}
		return out;
		*/
	}


	@Override
	public Vector<int[]> getDIMACS(Model m) {
		
        State cur = m.getCurrentStat();
		
		Vector<State> nexts = cur.getNexts();
		Vector<int []> exp = new Vector<int[]>();
		Vector<int []> pex = new Vector<int[]>();
		pex = this.F.getDIMACS(m);
		
		exp = and(pex,nexts.get(0).getAndVariables());
		for(int i = 1; i < nexts.size(); i++)
		{
			Vector<int[]> temp = and(pex,nexts.get(i).getAndVariables());
			
			exp = or(exp, temp);
		}
		
		//SAT.clean(exp);
		//SAT.printVec(exp);
		
		return exp;
		
		
	}
	
}
